es:ES, P:(E), R:(EE).
(e:E. Dec(P(e)))
 (e, e':E. Dec(R(e',e)))
 R => x,y. (x < y)
 Trans(E;x,y.R(x,y))
 (a, b, e:E.
 (x, y:E. x c e  y c e  P(x)  P(y)  (((x R y)  (x = y))  (y R x)))
  (R(e,a) & R(e,b))
  (P(e) & P(a) & P(b))
  (z:E. (R(e,z) & R(z,a) & P(z)))
  (z:E. (R(e,z) & R(z,b) & P(z)))
  (a = b))
 (m, m':E.
 P(m)  P(m')  (e:E. (e R m)  (P(e)))  (e:E. (e R m')  (P(e)))  (m = m'))
 (e, e':E. P(e)  P(e')  (((e R e')  (e = e'))  (e' R e))) 

latex

Definitions	R1 => R2, i  j , False, A  B, x,y. t(x;y), , {T}, A c B, x. t(x), t  T, x:A. B(x), A, P & Q, x f y, P  Q, x(s), Dec(P), P  Q, , x:A. B(x), e c e', R!, es-r-immediate-pred(es;R;e';e), Trans(T;x,y.E(x;y)), x(s1,s2), SWellFounded(R(x;y))
Lemmas	not-r-immediate-pred, decidable es-r-immediate-pred, false wf, nat wf, ge wf, nat properties, event system wf, es-E wf, decidable wf, rel implies wf, trans wf, es-causle wf, le wf, es-causl-swellfnd, not wf, es-causl wf, decidable cand, decidable existse-causl